[[NBG]]
# Class existence theorem schema

Let $\phi(X_{1},\dots,X_{n},Y_{1},\dots,Y_{m})$ be a [[predicative formula]].
Then #m/thm/set/nbg 
$$
\begin{align*}
\vdash (\exists \chood Z)(\forall \ehood x_{1}) \cdots (\forall \ehood x_{n})[(x_{1},\dots,x_{n}) \in Z \iff \varphi(x_{1},\dots,x_{n},Y_{1},\dots,Y_{m})]
\end{align*}
$$
for any classes $Y_{1},\dots,Y_{n}$.

> [!missing]- Proof
> #missing/proof

All of the [[NBG#Axioms of Class Existence]] are deductible from this theorem.

#
---
#state/develop | #lang/en | #SemBr